$\forall$$A$, $B$, $C$:Type, $f$:($B$$\rightarrow$$C$$\rightarrow$$C$), $k$:$C$, ${\it as}$:$A$ List, $g$:($A$$\rightarrow$($A$ List)$\rightarrow$$B$).
\\[0ex](ForHdTl\{$A$,$f$,$k$\} $h$::$t$ $\in$ ${\it as}$. $g$($h$,$t$)) $\in$ $C$